module Hacl.Test.Frodo

open FStar.HyperStack.All
open FStar.Mul

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer
open Lib.PrintBuffer

open Hacl.Impl.Frodo.KEM
open Hacl.Frodo.KEM
open Hacl.Impl.Matrix
open Hacl.Frodo.Random
open Frodo.Params

#reset-options "--z3rlimit 150 --max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Seq -Spec.Frodo.KEM.KeyGen -Spec.Frodo.KEM.Encaps -Spec.Frodo.KEM.Decaps'"

val test_frodo: 
  seed: lbytes 48ul ->
  ss_expected: ilbuffer uint8 crypto_bytes ->
  pk_expected: ilbuffer uint8 crypto_publickeybytes ->
  ct_expected: ilbuffer uint8 crypto_ciphertextbytes ->
  sk_expected: ilbuffer uint8 crypto_secretkeybytes ->
  Stack unit
    (requires
      fun h ->
        live h seed /\ live h ss_expected /\ live h pk_expected /\ live h ct_expected /\
        live h sk_expected)
    (ensures fun h0 r h1 -> True)
let test_frodo seed ss_expected pk_expected ct_expected sk_expected =
  recall state;
  randombytes_init_ seed;
  push_frame ();
  let pk_len = crypto_publickeybytes in
  let sk_len = crypto_secretkeybytes in
  let ct_len = crypto_ciphertextbytes in
  let ss_len = crypto_bytes in
  let pk = create pk_len (u8 0) in
  let sk = create sk_len (u8 0) in
  let ss1 = create ss_len (u8 0) in
  let ct = create ct_len (u8 0) in
  let ss2 = create ss_len (u8 0) in
  let _ = crypto_kem_keypair pk sk in
  let _ = crypto_kem_enc ct ss1 pk in
  let _ = crypto_kem_dec ss2 ct sk in
  print_compare_display pk_len pk pk_expected;
  print_compare_display sk_len sk sk_expected;
  print_compare_display ss_len ss1 ss_expected;
  print_compare_display ss_len ss2 ss_expected;
  print_compare_display ct_len ct ct_expected;
  pop_frame ()

/// Test1. FrodoKEM-64. CSHAKE128

inline_for_extraction noextract
val u8: n: nat{n < 0x100} -> uint8
let u8 n = u8 n

// The rest verifies for params_n = 64
// It expectedly fails for FrodoKEM-{640,976}.

let test1_ss_expected: b: ilbuffer uint8 crypto_bytes {recallable b} =
  [@ inline_let ]let l =
    [
      u8 0xdf; u8 0xc5; u8 0x2a; u8 0x95; u8 0x6c; u8 0xe4; u8 0xbc; u8 0xa5; u8 0x53; u8 0x70;
      u8 0x46; u8 0x5a; u8 0x7e; u8 0xf8; u8 0x4f; u8 0x68
    ]
  in
  createL_global l

let test1_pk_expected: b: ilbuffer uint8 crypto_publickeybytes {recallable b} =
  [@ inline_let ]let l =
    [
      u8 0x92; u8 0x44; u8 0x4d; u8 0x91; u8 0xa2; u8 0xad; u8 0xad; u8 0x05; u8 0x2c; u8 0xa2;
      u8 0x3d; u8 0xe5; u8 0xfb; u8 0x9d; u8 0xf9; u8 0xe1; u8 0x95; u8 0xe3; u8 0x8f; u8 0xc2;
      u8 0x21; u8 0xb8; u8 0xb8; u8 0x34; u8 0x14; u8 0xfb; u8 0xd3; u8 0xef; u8 0x7c; u8 0xa2;
      u8 0x6b; u8 0x36; u8 0x8c; u8 0x7b; u8 0x9d; u8 0x81; u8 0x78; u8 0xc9; u8 0x49; u8 0x64;
      u8 0x4d; u8 0x79; u8 0xfd; u8 0x8b; u8 0x19; u8 0xb9; u8 0x51; u8 0x4c; u8 0xce; u8 0x27;
      u8 0x4d; u8 0x64; u8 0xaa; u8 0xe0; u8 0x29; u8 0x69; u8 0x10; u8 0xaa; u8 0x9f; u8 0x49;
      u8 0xac; u8 0x16; u8 0x1d; u8 0xbc; u8 0x4e; u8 0xa0; u8 0x85; u8 0xf4; u8 0xf4; u8 0x58;
      u8 0x3a; u8 0xb9; u8 0xaa; u8 0xa9; u8 0xbd; u8 0x30; u8 0xf3; u8 0xc9; u8 0x1b; u8 0x6b;
      u8 0x4d; u8 0x26; u8 0xfe; u8 0x4b; u8 0x3e; u8 0xc1; u8 0x88; u8 0xeb; u8 0xde; u8 0x99;
      u8 0x0a; u8 0xa9; u8 0xb1; u8 0x27; u8 0xc0; u8 0x28; u8 0x96; u8 0x65; u8 0xfe; u8 0x3a;
      u8 0xf9; u8 0x0e; u8 0x67; u8 0x7a; u8 0x7f; u8 0x10; u8 0x4c; u8 0x16; u8 0xae; u8 0x2c;
      u8 0x0c; u8 0x72; u8 0x62; u8 0x5b; u8 0x4d; u8 0x3c; u8 0x12; u8 0x21; u8 0x9a; u8 0x7e;
      u8 0x8f; u8 0x07; u8 0x51; u8 0xe0; u8 0x86; u8 0x3e; u8 0x33; u8 0x98; u8 0x9b; u8 0x81;
      u8 0x2a; u8 0x96; u8 0x99; u8 0xe2; u8 0xf9; u8 0x99; u8 0x4f; u8 0x28; u8 0x0b; u8 0x76;
      u8 0xcb; u8 0x32; u8 0xb8; u8 0xea; u8 0x77; u8 0xad; u8 0xa3; u8 0xe9; u8 0xad; u8 0x82;
      u8 0x76; u8 0xe3; u8 0x8c; u8 0x4f; u8 0x71; u8 0x8f; u8 0xd8; u8 0xd4; u8 0xad; u8 0xb4;
      u8 0x5b; u8 0x3f; u8 0x84; u8 0xb3; u8 0xef; u8 0x91; u8 0x01; u8 0xb4; u8 0xaa; u8 0xfe;
      u8 0x7b; u8 0xda; u8 0xe3; u8 0x6b; u8 0x9e; u8 0x02; u8 0xc2; u8 0xb7; u8 0x35; u8 0xec;
      u8 0x77; u8 0x15; u8 0xe1; u8 0x13; u8 0x95; u8 0x68; u8 0xd4; u8 0x18; u8 0x44; u8 0x29;
      u8 0x78; u8 0x55; u8 0x47; u8 0xf5; u8 0x50; u8 0x98; u8 0x8e; u8 0xf3; u8 0x01; u8 0xa1;
      u8 0x71; u8 0xf5; u8 0x18; u8 0xa6; u8 0xd1; u8 0xfa; u8 0xac; u8 0x90; u8 0xe1; u8 0xa8;
      u8 0x4d; u8 0x83; u8 0xd7; u8 0xcd; u8 0xc5; u8 0x14; u8 0x1d; u8 0xce; u8 0x24; u8 0x9e;
      u8 0xc4; u8 0x7b; u8 0x15; u8 0x9f; u8 0x07; u8 0x3d; u8 0x85; u8 0xf6; u8 0x1b; u8 0x0d;
      u8 0xe6; u8 0xc1; u8 0x3f; u8 0x1e; u8 0x3f; u8 0x6c; u8 0x0a; u8 0xc7; u8 0x2d; u8 0xa4;
      u8 0x9d; u8 0xb2; u8 0x6e; u8 0x2c; u8 0xba; u8 0xb8; u8 0x6f; u8 0xab; u8 0x34; u8 0x3a;
      u8 0x48; u8 0xab; u8 0x2f; u8 0x75; u8 0xab; u8 0x48; u8 0x21; u8 0x8e; u8 0x59; u8 0x9d;
      u8 0xd0; u8 0xf7; u8 0xcd; u8 0x2d; u8 0xed; u8 0xc4; u8 0xb9; u8 0xae; u8 0x1b; u8 0x30;
      u8 0xf1; u8 0xc6; u8 0x94; u8 0x21; u8 0xa7; u8 0x81; u8 0x58; u8 0xcf; u8 0x0e; u8 0x7a;
      u8 0xf0; u8 0xb5; u8 0x44; u8 0x42; u8 0x1a; u8 0xd4; u8 0x22; u8 0xfa; u8 0x18; u8 0x0d;
      u8 0x2c; u8 0x05; u8 0xd3; u8 0x74; u8 0xeb; u8 0x90; u8 0x11; u8 0x25; u8 0xaf; u8 0x00;
      u8 0x3e; u8 0xe7; u8 0xbe; u8 0xf1; u8 0x1e; u8 0xaf; u8 0x6d; u8 0xd0; u8 0x7f; u8 0xa4;
      u8 0x12; u8 0xcf; u8 0x4f; u8 0xc4; u8 0x65; u8 0xaa; u8 0x07; u8 0x73; u8 0x5f; u8 0x22;
      u8 0xa0; u8 0x32; u8 0xd4; u8 0xd5; u8 0xe5; u8 0x28; u8 0x47; u8 0x2e; u8 0xb5; u8 0xc1;
      u8 0x2d; u8 0x58; u8 0xc2; u8 0xe9; u8 0x83; u8 0xcd; u8 0x41; u8 0xa0; u8 0x82; u8 0x63;
      u8 0x92; u8 0x76; u8 0xc3; u8 0x51; u8 0x05; u8 0xf0; u8 0x6f; u8 0x18; u8 0xed; u8 0xb7;
      u8 0x7b; u8 0x87; u8 0xcb; u8 0x90; u8 0x16; u8 0x63; u8 0x3b; u8 0x67; u8 0xc1; u8 0x3a;
      u8 0xbb; u8 0x66; u8 0x0b; u8 0xcd; u8 0x9d; u8 0x9b; u8 0x38; u8 0x7f; u8 0xa1; u8 0x91;
      u8 0x14; u8 0x07; u8 0x7f; u8 0xcf; u8 0x1f; u8 0x11; u8 0x31; u8 0xf7; u8 0x95; u8 0x89;
      u8 0xf7; u8 0x35; u8 0x34; u8 0x11; u8 0xa5; u8 0x5c; u8 0xab; u8 0x70; u8 0x05; u8 0xdd;
      u8 0x38; u8 0xc1; u8 0x7a; u8 0x42; u8 0x89; u8 0x6d; u8 0x13; u8 0xdc; u8 0x16; u8 0xaa;
      u8 0xbc; u8 0x43; u8 0xc2; u8 0x20; u8 0x0f; u8 0xd2; u8 0x21; u8 0x3e; u8 0x15; u8 0x76;
      u8 0x6f; u8 0x82; u8 0xef; u8 0x29; u8 0x96; u8 0x4c; u8 0xd5; u8 0xf4; u8 0x79; u8 0x3a;
      u8 0x29; u8 0x54; u8 0xab; u8 0xc3; u8 0x37; u8 0xbb; u8 0x8c; u8 0x2a; u8 0x86; u8 0x5d;
      u8 0x76; u8 0x31; u8 0xc8; u8 0xc1; u8 0x30; u8 0x47; u8 0x7a; u8 0xce; u8 0x37; u8 0xf0;
      u8 0xe0; u8 0xe3; u8 0x64; u8 0x6a; u8 0xdd; u8 0xb1; u8 0x7d; u8 0x59; u8 0x17; u8 0xee;
      u8 0xd5; u8 0xfb; u8 0xa9; u8 0x1b; u8 0xd6; u8 0x1f; u8 0x70; u8 0x21; u8 0xa7; u8 0xdc;
      u8 0x55; u8 0x63; u8 0xff; u8 0xdd; u8 0xe5; u8 0xb5; u8 0x52; u8 0xc5; u8 0x7d; u8 0x41;
      u8 0x7e; u8 0x8a; u8 0xdf; u8 0xc1; u8 0xf6; u8 0x03; u8 0x8f; u8 0xc7; u8 0x52; u8 0xa3;
      u8 0xc7; u8 0x66; u8 0x79; u8 0x55; u8 0xed; u8 0x0e; u8 0x40; u8 0x59; u8 0xbc; u8 0x60;
      u8 0x13; u8 0x86; u8 0xb4; u8 0x88; u8 0x8c; u8 0xba; u8 0x9b; u8 0x80; u8 0x8a; u8 0x2b;
      u8 0x4e; u8 0x80; u8 0x92; u8 0xe1; u8 0xd2; u8 0x84; u8 0x93; u8 0xb6; u8 0xc8; u8 0xb3;
      u8 0x23; u8 0x1d; u8 0xd3; u8 0xf7; u8 0xdd; u8 0xa6; u8 0x39; u8 0x1a; u8 0x65; u8 0x08;
      u8 0x0f; u8 0x95; u8 0x78; u8 0x89; u8 0xaf; u8 0xab; u8 0xb9; u8 0x9d; u8 0x32; u8 0x89;
      u8 0x82; u8 0x07; u8 0xf2; u8 0x1d; u8 0xc0; u8 0xba; u8 0x30; u8 0x01; u8 0x42; u8 0x9a;
      u8 0xcc; u8 0x8e; u8 0x16; u8 0x7a; u8 0xc0; u8 0xd7; u8 0x4a; u8 0x91; u8 0xe0; u8 0x46;
      u8 0xf5; u8 0xae; u8 0xe0; u8 0xed; u8 0x0a; u8 0x2c; u8 0xe1; u8 0xaf; u8 0x40; u8 0xf1;
      u8 0x4d; u8 0x18; u8 0x71; u8 0x5e; u8 0xd3; u8 0x6c; u8 0x9c; u8 0x52; u8 0x70; u8 0xfd;
      u8 0xd2; u8 0xac; u8 0x05; u8 0xf6; u8 0xcb; u8 0x22; u8 0x9f; u8 0x04; u8 0x8d; u8 0xd0;
      u8 0x25; u8 0xe1; u8 0xfb; u8 0xed; u8 0x19; u8 0x7e; u8 0x65; u8 0x51; u8 0x60; u8 0xcc;
      u8 0x88; u8 0xce; u8 0xda; u8 0xf5; u8 0xad; u8 0xfd; u8 0x63; u8 0xd2; u8 0x62; u8 0x3f;
      u8 0x98; u8 0x05; u8 0xbf; u8 0xd9; u8 0xae; u8 0x16; u8 0x90; u8 0xdb; u8 0x1e; u8 0x15;
      u8 0x2e; u8 0xb0; u8 0xcd; u8 0x95; u8 0x8c; u8 0x27; u8 0x6a; u8 0xd9; u8 0x1b; u8 0xc1;
      u8 0xdd; u8 0x02; u8 0xa9; u8 0x92; u8 0x9a; u8 0x9e; u8 0x2b; u8 0x25; u8 0xeb; u8 0x82;
      u8 0x65; u8 0xcf; u8 0x5e; u8 0x25; u8 0x8c; u8 0x5e; u8 0xc3; u8 0x2a; u8 0x85; u8 0x50;
      u8 0x67; u8 0x78; u8 0x6c; u8 0xe5; u8 0x8f; u8 0xdb; u8 0x56; u8 0xd3; u8 0x73; u8 0x64;
      u8 0x83; u8 0xaa; u8 0xe6; u8 0x97; u8 0x2d; u8 0x90; u8 0x9c; u8 0xb3; u8 0x59; u8 0xf5;
      u8 0xee; u8 0x59; u8 0xe3; u8 0x05; u8 0xb1; u8 0xa1; u8 0x45; u8 0x4c; u8 0xcf; u8 0x94;
      u8 0x3e; u8 0x5c; u8 0x15; u8 0x06; u8 0xf9; u8 0x5c; u8 0xc3; u8 0x82; u8 0x22; u8 0x71;
      u8 0x2b; u8 0x42; u8 0xb5; u8 0xd5; u8 0x44; u8 0x8f; u8 0xf8; u8 0x64; u8 0x54; u8 0x75;
      u8 0x03; u8 0xcf; u8 0xdd; u8 0x91; u8 0x6b; u8 0x05; u8 0x09; u8 0x24; u8 0x7f; u8 0xd5;
      u8 0x97; u8 0x3e; u8 0xa4; u8 0x7c; u8 0x65; u8 0x0a; u8 0x42; u8 0x6b; u8 0x64; u8 0xa2;
      u8 0xd8; u8 0x81; u8 0x4f; u8 0xc0; u8 0xec; u8 0xd8; u8 0x79; u8 0x4c; u8 0xcb; u8 0x9c;
      u8 0x27; u8 0xbc; u8 0x60; u8 0x6f; u8 0xe2; u8 0x49; u8 0x9b; u8 0x44; u8 0x93; u8 0x6d;
      u8 0xa4; u8 0x74; u8 0x04; u8 0x1c; u8 0x81; u8 0xf9; u8 0x01; u8 0x8f; u8 0xd2; u8 0x4d;
      u8 0xad; u8 0x07; u8 0x9a; u8 0xbb; u8 0x11; u8 0xc8; u8 0x76; u8 0x64; u8 0x29; u8 0xfe;
      u8 0xa4; u8 0x1a; u8 0x25; u8 0x05; u8 0x4a; u8 0xaf; u8 0x59; u8 0xa9; u8 0x88; u8 0xf7;
      u8 0x73; u8 0x12; u8 0x60; u8 0xd4; u8 0x12; u8 0x01; u8 0x68; u8 0xf5; u8 0xbe; u8 0xc5;
      u8 0xb2; u8 0x7b; u8 0xdc; u8 0xeb; u8 0x96; u8 0xec; u8 0x43; u8 0x5d; u8 0xc2; u8 0x07;
      u8 0xb4; u8 0x1d; u8 0xf7; u8 0x78; u8 0xa7; u8 0x82; u8 0x8d; u8 0x10; u8 0x0b; u8 0x90;
      u8 0xeb; u8 0x5c; u8 0x1e; u8 0x49; u8 0x7b; u8 0xdd; u8 0x56; u8 0xc7; u8 0x5f; u8 0x0f;
      u8 0x8f; u8 0x9a; u8 0x21; u8 0xcf; u8 0xa4; u8 0x63; u8 0x20; u8 0x0c; u8 0xe5; u8 0xf7;
      u8 0xc2; u8 0xdf; u8 0xf1; u8 0xec; u8 0xf3; u8 0x94; u8 0x5b; u8 0xad; u8 0x29; u8 0xdd;
      u8 0x0b; u8 0x43; u8 0x19; u8 0xab; u8 0x93; u8 0xec; u8 0x7d; u8 0x50; u8 0x6b; u8 0x67;
      u8 0xf5; u8 0x2f; u8 0xf1; u8 0xe7; u8 0x4b; u8 0xe2; u8 0x35; u8 0x41; u8 0x47; u8 0xd8;
      u8 0xcf; u8 0x9a; u8 0xbb; u8 0x38; u8 0x3a; u8 0x37; u8 0xc3; u8 0x61; u8 0x43; u8 0xa4;
      u8 0x41; u8 0xab; u8 0x4d; u8 0x9b; u8 0xd9; u8 0xbf; u8 0x19; u8 0x6e; u8 0x66; u8 0xa1;
      u8 0xfd; u8 0xef; u8 0x54; u8 0x6f; u8 0xef; u8 0x1e; u8 0xe0; u8 0x26; u8 0xab; u8 0xe3;
      u8 0xf5; u8 0xe7; u8 0x22; u8 0xd0; u8 0x84; u8 0x6e; u8 0x78; u8 0x90; u8 0x70; u8 0xc3;
      u8 0x87; u8 0x6a; u8 0x68; u8 0xb8; u8 0x5f; u8 0x80; u8 0x10; u8 0xb3; u8 0x8f; u8 0x56;
      u8 0xff; u8 0x16; u8 0xf9; u8 0x88; u8 0x67; u8 0x1a; u8 0x51; u8 0x3c; u8 0xf8; u8 0x27;
      u8 0x40; u8 0xbb; u8 0x69; u8 0x6e; u8 0xcb; u8 0x80; u8 0xa4; u8 0x0d; u8 0xb6; u8 0xb2;
      u8 0x66; u8 0xbd; u8 0xa2; u8 0xcb; u8 0xfe; u8 0xd7; u8 0x67; u8 0x5f; u8 0xfa; u8 0x85;
      u8 0xd0; u8 0x98; u8 0x1e; u8 0x5d; u8 0x35; u8 0x01; u8 0x91; u8 0x3f; u8 0x91; u8 0x46;
      u8 0xac; u8 0xcd; u8 0x82; u8 0xd3; u8 0xe1; u8 0x5c; u8 0x53; u8 0x66; u8 0xa7; u8 0xa1;
      u8 0x00; u8 0xd5; u8 0x34; u8 0x3f; u8 0x1e; u8 0x1e; u8 0x0f; u8 0x1c; u8 0xef; u8 0x5d;
      u8 0x2e; u8 0x79; u8 0x28; u8 0x02; u8 0xbe; u8 0x9b; u8 0x8b; u8 0xfa; u8 0x5a; u8 0x0a;
      u8 0xf3; u8 0xfc; u8 0x8c; u8 0xdc; u8 0xbd; u8 0xa3; u8 0xb6; u8 0xd3; u8 0x5b; u8 0xe0;
      u8 0xfb; u8 0xee; u8 0x63; u8 0xd3; u8 0x72; u8 0x5a
    ]
  in
  createL_global l

let test1_ct_expected: b: ilbuffer uint8 crypto_ciphertextbytes {recallable b} =
  [@ inline_let ]let l =
    [
      u8 0x9d; u8 0x0e; u8 0x6e; u8 0xec; u8 0xc3; u8 0xd0; u8 0xa5; u8 0x9f; u8 0xba; u8 0xf9;
      u8 0xfb; u8 0xc9; u8 0x30; u8 0x42; u8 0x58; u8 0x2a; u8 0xf6; u8 0x5b; u8 0x14; u8 0x49;
      u8 0xec; u8 0x17; u8 0x96; u8 0xac; u8 0x33; u8 0x1e; u8 0xe9; u8 0x13; u8 0x66; u8 0x01;
      u8 0x88; u8 0x3a; u8 0x1a; u8 0x86; u8 0x1c; u8 0x54; u8 0xeb; u8 0x12; u8 0xbe; u8 0x84;
      u8 0x28; u8 0x5e; u8 0xbe; u8 0x62; u8 0x6a; u8 0x2b; u8 0xe3; u8 0xc7; u8 0xe2; u8 0xee;
      u8 0x0c; u8 0x1d; u8 0x08; u8 0xbd; u8 0xd0; u8 0xe0; u8 0x0c; u8 0xef; u8 0xe0; u8 0x23;
      u8 0x5d; u8 0x60; u8 0xea; u8 0x22; u8 0x39; u8 0x03; u8 0x0b; u8 0xce; u8 0xf3; u8 0xe3;
      u8 0xfc; u8 0x96; u8 0xde; u8 0xe2; u8 0xbf; u8 0x5d; u8 0x41; u8 0x59; u8 0x43; u8 0xce;
      u8 0xe6; u8 0x1a; u8 0x79; u8 0xa3; u8 0x76; u8 0x5e; u8 0xe7; u8 0x8c; u8 0x2e; u8 0x3d;
      u8 0x74; u8 0x14; u8 0x3d; u8 0xa3; u8 0x34; u8 0xcf; u8 0xac; u8 0x56; u8 0x34; u8 0x73;
      u8 0x5b; u8 0xcc; u8 0xd3; u8 0xd2; u8 0x8b; u8 0xa2; u8 0x4b; u8 0x57; u8 0xe3; u8 0x62;
      u8 0x09; u8 0xe3; u8 0x19; u8 0xc0; u8 0x21; u8 0x01; u8 0x98; u8 0x82; u8 0x60; u8 0x58;
      u8 0x4c; u8 0x63; u8 0x7d; u8 0xbc; u8 0xe0; u8 0x2e; u8 0x86; u8 0x08; u8 0x7f; u8 0xf1;
      u8 0x79; u8 0x7d; u8 0xac; u8 0x53; u8 0x81; u8 0xfd; u8 0xed; u8 0xe5; u8 0x98; u8 0x03;
      u8 0x03; u8 0x09; u8 0x78; u8 0x0d; u8 0xe0; u8 0x18; u8 0x24; u8 0xed; u8 0xe6; u8 0x58;
      u8 0x22; u8 0xd6; u8 0x50; u8 0xae; u8 0x1b; u8 0x32; u8 0x8d; u8 0x51; u8 0x81; u8 0xc1;
      u8 0x7d; u8 0xc4; u8 0xa9; u8 0x69; u8 0xc3; u8 0x13; u8 0xe2; u8 0xbb; u8 0x27; u8 0x8e;
      u8 0x90; u8 0x23; u8 0xe1; u8 0xae; u8 0xd8; u8 0xdb; u8 0xa6; u8 0x89; u8 0xfb; u8 0xac;
      u8 0xc6; u8 0x39; u8 0xb9; u8 0xf4; u8 0xa5; u8 0x1b; u8 0x43; u8 0x22; u8 0x19; u8 0x01;
      u8 0x37; u8 0x7a; u8 0x0a; u8 0xf2; u8 0xf3; u8 0x22; u8 0xc5; u8 0x41; u8 0xfe; u8 0x37;
      u8 0x01; u8 0xaa; u8 0x49; u8 0x1e; u8 0xad; u8 0xf5; u8 0x57; u8 0x20; u8 0x66; u8 0x01;
      u8 0xfe; u8 0xc7; u8 0x6c; u8 0xe5; u8 0xe1; u8 0x83; u8 0xcc; u8 0xf1; u8 0x1d; u8 0x4f;
      u8 0xf2; u8 0x4b; u8 0xdf; u8 0xcc; u8 0xdb; u8 0x66; u8 0xe0; u8 0x20; u8 0x89; u8 0x02;
      u8 0x24; u8 0xda; u8 0xb7; u8 0x85; u8 0x81; u8 0x59; u8 0x3a; u8 0x02; u8 0xac; u8 0x4f;
      u8 0x13; u8 0xa6; u8 0x82; u8 0xc2; u8 0x78; u8 0x7d; u8 0x2d; u8 0xb6; u8 0xc6; u8 0xdc;
      u8 0x5e; u8 0x15; u8 0x8d; u8 0x24; u8 0xba; u8 0x6a; u8 0x35; u8 0x13; u8 0x12; u8 0x7d;
      u8 0xec; u8 0xba; u8 0x5f; u8 0x8f; u8 0x02; u8 0x51; u8 0xcf; u8 0x74; u8 0x26; u8 0x47;
      u8 0x11; u8 0x6f; u8 0xa9; u8 0xfc; u8 0x1d; u8 0x1d; u8 0x23; u8 0x0d; u8 0x25; u8 0xd8;
      u8 0xf2; u8 0x6b; u8 0x8c; u8 0x3b; u8 0xf0; u8 0xd0; u8 0xcc; u8 0xf6; u8 0xe5; u8 0x3d;
      u8 0x58; u8 0x4a; u8 0x88; u8 0xd4; u8 0x48; u8 0xfb; u8 0x49; u8 0xff; u8 0x87; u8 0x2f;
      u8 0x1a; u8 0xc1; u8 0xdd; u8 0x58; u8 0xff; u8 0x55; u8 0x09; u8 0x09; u8 0xf1; u8 0x10;
      u8 0x86; u8 0xa0; u8 0x42; u8 0x98; u8 0x23; u8 0x22; u8 0x43; u8 0x60; u8 0xb3; u8 0xe8;
      u8 0xf2; u8 0xe9; u8 0xcc; u8 0x1c; u8 0xbe; u8 0x04; u8 0x1a; u8 0xf5; u8 0x80; u8 0x41;
      u8 0x20; u8 0x1b; u8 0x78; u8 0x5a; u8 0x15; u8 0x7f; u8 0xbb; u8 0xce; u8 0x85; u8 0xbc;
      u8 0xb8; u8 0x69; u8 0x89; u8 0x60; u8 0xf2; u8 0xf6; u8 0x68; u8 0x85; u8 0x23; u8 0x84;
      u8 0x49; u8 0xa5; u8 0x79; u8 0xbe; u8 0xa7; u8 0x32; u8 0x98; u8 0xa9; u8 0x50; u8 0xb3;
      u8 0x32; u8 0xec; u8 0x8e; u8 0x44; u8 0xf5; u8 0xa9; u8 0x55; u8 0x8b; u8 0x41; u8 0x70;
      u8 0x5f; u8 0x88; u8 0x88; u8 0x90; u8 0x9f; u8 0x13; u8 0x4c; u8 0x8e; u8 0x5a; u8 0x92;
      u8 0xd3; u8 0x2d; u8 0x48; u8 0x49; u8 0x65; u8 0x3c; u8 0x06; u8 0x41; u8 0x9e; u8 0x1f;
      u8 0xdb; u8 0xc0; u8 0x25; u8 0x4f; u8 0xbb; u8 0x20; u8 0x98; u8 0x11; u8 0x2a; u8 0xa5;
      u8 0x5f; u8 0xc9; u8 0x1f; u8 0x66; u8 0xe7; u8 0xbc; u8 0x3b; u8 0x68; u8 0xda; u8 0xb9;
      u8 0x47; u8 0xa1; u8 0x62; u8 0x59; u8 0xb4; u8 0x72; u8 0xb4; u8 0xa8; u8 0x82; u8 0xf6;
      u8 0x7c; u8 0xc7; u8 0xec; u8 0x9f; u8 0xba; u8 0xc5; u8 0x5f; u8 0xf7; u8 0xdb; u8 0x4d;
      u8 0xe1; u8 0x9c; u8 0xf1; u8 0xcc; u8 0x1d; u8 0x4d; u8 0x04; u8 0xa9; u8 0x2f; u8 0xeb;
      u8 0x16; u8 0x1d; u8 0x0d; u8 0xfa; u8 0x57; u8 0xc0; u8 0x94; u8 0x8f; u8 0xbc; u8 0x11;
      u8 0x98; u8 0x44; u8 0xab; u8 0x4c; u8 0x68; u8 0xc4; u8 0x9a; u8 0x51; u8 0xed; u8 0x97;
      u8 0x6b; u8 0x12; u8 0x2f; u8 0xf2; u8 0xda; u8 0x68; u8 0x33; u8 0xd3; u8 0x24; u8 0x53;
      u8 0x11; u8 0x9c; u8 0x32; u8 0xc6; u8 0xb2; u8 0xc1; u8 0x3a; u8 0x76; u8 0xe9; u8 0x93;
      u8 0x2c; u8 0xd7; u8 0xd9; u8 0xec; u8 0x60; u8 0x20; u8 0x39; u8 0xe7; u8 0x7f; u8 0x26;
      u8 0x5c; u8 0xd4; u8 0xc7; u8 0xf0; u8 0xdf; u8 0xc4; u8 0xe9; u8 0x7b; u8 0x09; u8 0xbf;
      u8 0xfa; u8 0xbd; u8 0xce; u8 0x8c; u8 0x1a; u8 0x84; u8 0xae; u8 0xfd; u8 0x41; u8 0x9c;
      u8 0x9c; u8 0x02; u8 0x69; u8 0x34; u8 0xf4; u8 0x27; u8 0x9d; u8 0x87; u8 0x23; u8 0xf9;
      u8 0x69; u8 0xa8; u8 0xc1; u8 0x24; u8 0xca; u8 0x44; u8 0x9b; u8 0x6c; u8 0x4a; u8 0x23;
      u8 0x41; u8 0x17; u8 0x9f; u8 0x82; u8 0xfe; u8 0x74; u8 0xe5; u8 0x3a; u8 0x6e; u8 0x15;
      u8 0xbf; u8 0xeb; u8 0x8f; u8 0xb6; u8 0x51; u8 0x54; u8 0x86; u8 0xc5; u8 0xf7; u8 0xea;
      u8 0x2e; u8 0xbc; u8 0x63; u8 0x2a; u8 0x18; u8 0x85; u8 0x72; u8 0x4d; u8 0x6f; u8 0x56;
      u8 0x3b; u8 0xa1; u8 0x66; u8 0x73; u8 0xfa; u8 0x59; u8 0x8a; u8 0xec; u8 0xc1; u8 0x6d;
      u8 0x49; u8 0xc3; u8 0x30; u8 0xf1; u8 0x0e; u8 0x3f; u8 0x07; u8 0xb3; u8 0x4d; u8 0x58;
      u8 0x36; u8 0xe8; u8 0xeb; u8 0xb2; u8 0xef; u8 0x9d; u8 0x84; u8 0x1e; u8 0x5d; u8 0xbc;
      u8 0xad; u8 0xa6; u8 0x4a; u8 0x46; u8 0x6f; u8 0x91; u8 0xce; u8 0x14; u8 0xa5; u8 0x85;
      u8 0x69; u8 0x33; u8 0x86; u8 0xa9; u8 0x57; u8 0x85; u8 0x15; u8 0x08; u8 0xee; u8 0x76;
      u8 0x3b; u8 0x6b; u8 0x64; u8 0x74; u8 0xe4; u8 0xf7; u8 0x4d; u8 0x0f; u8 0xd5; u8 0x92;
      u8 0x43; u8 0x12; u8 0xae; u8 0xbb; u8 0x37; u8 0xc4; u8 0x13; u8 0x92; u8 0xe6; u8 0xd6;
      u8 0x46; u8 0xc0; u8 0xa0; u8 0xa7; u8 0xa8; u8 0xf2; u8 0x39; u8 0x45; u8 0x72; u8 0xac;
      u8 0x5c; u8 0xa9; u8 0x94; u8 0x88; u8 0x2a; u8 0xaa; u8 0x23; u8 0x5c; u8 0x49; u8 0x86;
      u8 0x2a; u8 0xe4; u8 0x7b; u8 0xb1; u8 0xc1; u8 0x4f; u8 0xae; u8 0x9a; u8 0xa2; u8 0x13;
      u8 0x15; u8 0xf9; u8 0x20; u8 0x39; u8 0x85; u8 0x0a; u8 0x3c; u8 0x9d; u8 0xc6; u8 0x16;
      u8 0x3e; u8 0x0c; u8 0xfb; u8 0xc8; u8 0xff; u8 0xcc; u8 0x3d; u8 0xbf; u8 0x11; u8 0x24;
      u8 0x79; u8 0xe1; u8 0xea; u8 0xf8; u8 0xb7; u8 0x98; u8 0xd6; u8 0x35; u8 0xbc; u8 0xb5;
      u8 0x78; u8 0x7d; u8 0xcd; u8 0x89; u8 0x70; u8 0xb2; u8 0xba; u8 0x53; u8 0xea; u8 0x38;
      u8 0xa0; u8 0xa4; u8 0xc1; u8 0x49; u8 0xc1; u8 0xf5; u8 0x6c; u8 0xa7; u8 0x04; u8 0x81;
      u8 0x12; u8 0x99; u8 0x37; u8 0x21; u8 0x93; u8 0xdb; u8 0x0e; u8 0x38; u8 0xc3; u8 0xd8;
      u8 0x4a; u8 0xc7; u8 0xf6; u8 0x5d; u8 0x5d; u8 0x1f; u8 0xd1; u8 0x58; u8 0xd7; u8 0xdf;
      u8 0x86; u8 0xa0; u8 0xcd; u8 0xfc; u8 0xb5; u8 0xf1; u8 0xae; u8 0x0f; u8 0x60; u8 0x6a;
      u8 0x39; u8 0x73; u8 0xe4; u8 0x70; u8 0xa7; u8 0xf0; u8 0x77; u8 0x59; u8 0x9d; u8 0x0c;
      u8 0x0e; u8 0x14; u8 0xa1; u8 0x5e; u8 0xd5; u8 0xe8; u8 0x6e; u8 0x82; u8 0x8c; u8 0xf9;
      u8 0x94; u8 0x61; u8 0xb6; u8 0x2c; u8 0x0e; u8 0x26; u8 0x59; u8 0xdd; u8 0xe6; u8 0x79;
      u8 0xdc; u8 0x21; u8 0xcf; u8 0xe1; u8 0x5d; u8 0x69; u8 0xff; u8 0x0e; u8 0x93; u8 0x28;
      u8 0x3a; u8 0x86; u8 0xa5; u8 0x47; u8 0xd8; u8 0xac; u8 0x50; u8 0x81; u8 0x2c; u8 0x95;
      u8 0x67; u8 0x5d; u8 0xf7; u8 0x27; u8 0xfd; u8 0xa5; u8 0x20; u8 0xc3; u8 0x85; u8 0x6d;
      u8 0x4c; u8 0xf2; u8 0xd0; u8 0xe6; u8 0x9f; u8 0x73; u8 0xef; u8 0xd1; u8 0x7f; u8 0x84;
      u8 0xd5; u8 0xa1; u8 0x0c; u8 0x87; u8 0xbe; u8 0xef; u8 0xcc; u8 0xf8; u8 0xb0; u8 0x3f;
      u8 0x7b; u8 0x30; u8 0x43; u8 0x6a; u8 0xd0; u8 0x5d; u8 0xaf; u8 0x78; u8 0x89; u8 0x19;
      u8 0x03; u8 0x09; u8 0xee; u8 0xe1; u8 0x60; u8 0x7e; u8 0xf0; u8 0x74; u8 0x87; u8 0x22;
      u8 0xc1; u8 0x6d; u8 0x8e; u8 0x20; u8 0x34; u8 0x82; u8 0x87; u8 0x23; u8 0x45; u8 0x17;
      u8 0xf2; u8 0x2d; u8 0x95; u8 0xc4; u8 0xc5; u8 0x42; u8 0xb9; u8 0xa1; u8 0x07; u8 0x4c;
      u8 0x89; u8 0xd7; u8 0xf2; u8 0x9b; u8 0xdf; u8 0xf3; u8 0xac; u8 0xae; u8 0x9c; u8 0x13;
      u8 0x5d; u8 0x07; u8 0xd5; u8 0x7e; u8 0x66; u8 0x34; u8 0xd6; u8 0x15; u8 0x6e; u8 0xd4;
      u8 0x5d; u8 0x50; u8 0x7d; u8 0xab; u8 0x17; u8 0x02; u8 0x58; u8 0x95; u8 0xaf; u8 0xc6;
      u8 0x17; u8 0x2f; u8 0xfc; u8 0xdc; u8 0x5a; u8 0xbe; u8 0x5a; u8 0xcb; u8 0x50; u8 0x85;
      u8 0x7d; u8 0x7d; u8 0x3b; u8 0x2a; u8 0xbb; u8 0x29; u8 0xd6; u8 0xff; u8 0xec; u8 0x4c;
      u8 0xcf; u8 0x8e; u8 0xfa; u8 0xc1; u8 0xb5; u8 0x97; u8 0x15; u8 0x07; u8 0xe8; u8 0x62;
      u8 0x27; u8 0x1d; u8 0x28; u8 0x3d; u8 0x81; u8 0x5a; u8 0xf0; u8 0x0d; u8 0x98; u8 0x49;
      u8 0x33; u8 0x26; u8 0xdc; u8 0x56; u8 0x28; u8 0x88; u8 0xdd; u8 0x1c; u8 0x98; u8 0x52;
      u8 0xca; u8 0x99; u8 0xbf; u8 0xbc; u8 0xc2; u8 0xf4; u8 0x29; u8 0x85; u8 0x5f; u8 0x5c;
      u8 0x56; u8 0x53; u8 0xa4; u8 0x03; u8 0x02; u8 0xca; u8 0x50; u8 0x45; u8 0xed; u8 0x96;
      u8 0x10; u8 0x42; u8 0x94; u8 0x5a; u8 0x14; u8 0x4e; u8 0xb8; u8 0x59; u8 0x81; u8 0x04;
      u8 0x9a; u8 0x3e; u8 0xae; u8 0x63; u8 0xf6; u8 0xcc; u8 0x17; u8 0xca; u8 0xb3; u8 0xf9;
      u8 0x32; u8 0xc6; u8 0x7e; u8 0x56; u8 0x3b; u8 0x7c; u8 0xa4; u8 0xf1; u8 0x2c; u8 0x37;
      u8 0xb2; u8 0x6e; u8 0x78; u8 0x09; u8 0x9b; u8 0x52; u8 0x0e; u8 0x55; u8 0xfd; u8 0xc2;
      u8 0xe2; u8 0x7c; u8 0xc4; u8 0x95; u8 0xad; u8 0xe5; u8 0x20; u8 0x6a; u8 0x12; u8 0x47;
      u8 0x41; u8 0x7e; u8 0x02; u8 0x88; u8 0x1a; u8 0x93; u8 0xe9; u8 0x5d; u8 0x86; u8 0x4f;
      u8 0x53; u8 0x17; u8 0x76; u8 0x33; u8 0x15; u8 0x2e; u8 0x75; u8 0x3b; u8 0x77; u8 0x9b;
      u8 0x00; u8 0x1d; u8 0xc1; u8 0x27; u8 0xbb; u8 0x88; u8 0x73; u8 0x53; u8 0x71; u8 0xc7;
      u8 0x7b; u8 0xa4; u8 0x78; u8 0xe9; u8 0xdf; u8 0x49; u8 0xe5; u8 0xcc; u8 0xb9; u8 0xc5;
      u8 0x91; u8 0x10; u8 0x5c; u8 0x3c; u8 0xd9; u8 0xb5; u8 0x98; u8 0xb3; u8 0x63; u8 0x4c;
      u8 0xc8; u8 0x2f; u8 0x24; u8 0x16; u8 0x5d; u8 0xad; u8 0x11; u8 0x83; u8 0x9b; u8 0xe1;
      u8 0xb8; u8 0x1e; u8 0x11; u8 0xd9; u8 0x45; u8 0xe1; u8 0xd6; u8 0x90; u8 0x91; u8 0xaa;
      u8 0x94; u8 0x8a; u8 0xb3; u8 0xc0; u8 0x4d; u8 0x7a; u8 0x76; u8 0xcb; u8 0x44; u8 0x02;
      u8 0x3a; u8 0x8d; u8 0x9a; u8 0x18; u8 0xbc; u8 0x6c
    ]
  in
  createL_global l

let test1_sk_expected: b: ilbuffer uint8 crypto_secretkeybytes {recallable b} =
  [@ inline_let ]let l: list uint8 =
    [
      u8 0x4b; u8 0x62; u8 0x2d; u8 0xe1; u8 0x35; u8 0x01; u8 0x19; u8 0xc4; u8 0x5a; u8 0x9f;
      u8 0x2e; u8 0x2e; u8 0xf3; u8 0xdc; u8 0x5d; u8 0xf5; u8 0x92; u8 0x44; u8 0x4d; u8 0x91;
      u8 0xa2; u8 0xad; u8 0xad; u8 0x05; u8 0x2c; u8 0xa2; u8 0x3d; u8 0xe5; u8 0xfb; u8 0x9d;
      u8 0xf9; u8 0xe1; u8 0x95; u8 0xe3; u8 0x8f; u8 0xc2; u8 0x21; u8 0xb8; u8 0xb8; u8 0x34;
      u8 0x14; u8 0xfb; u8 0xd3; u8 0xef; u8 0x7c; u8 0xa2; u8 0x6b; u8 0x36; u8 0x8c; u8 0x7b;
      u8 0x9d; u8 0x81; u8 0x78; u8 0xc9; u8 0x49; u8 0x64; u8 0x4d; u8 0x79; u8 0xfd; u8 0x8b;
      u8 0x19; u8 0xb9; u8 0x51; u8 0x4c; u8 0xce; u8 0x27; u8 0x4d; u8 0x64; u8 0xaa; u8 0xe0;
      u8 0x29; u8 0x69; u8 0x10; u8 0xaa; u8 0x9f; u8 0x49; u8 0xac; u8 0x16; u8 0x1d; u8 0xbc;
      u8 0x4e; u8 0xa0; u8 0x85; u8 0xf4; u8 0xf4; u8 0x58; u8 0x3a; u8 0xb9; u8 0xaa; u8 0xa9;
      u8 0xbd; u8 0x30; u8 0xf3; u8 0xc9; u8 0x1b; u8 0x6b; u8 0x4d; u8 0x26; u8 0xfe; u8 0x4b;
      u8 0x3e; u8 0xc1; u8 0x88; u8 0xeb; u8 0xde; u8 0x99; u8 0x0a; u8 0xa9; u8 0xb1; u8 0x27;
      u8 0xc0; u8 0x28; u8 0x96; u8 0x65; u8 0xfe; u8 0x3a; u8 0xf9; u8 0x0e; u8 0x67; u8 0x7a;
      u8 0x7f; u8 0x10; u8 0x4c; u8 0x16; u8 0xae; u8 0x2c; u8 0x0c; u8 0x72; u8 0x62; u8 0x5b;
      u8 0x4d; u8 0x3c; u8 0x12; u8 0x21; u8 0x9a; u8 0x7e; u8 0x8f; u8 0x07; u8 0x51; u8 0xe0;
      u8 0x86; u8 0x3e; u8 0x33; u8 0x98; u8 0x9b; u8 0x81; u8 0x2a; u8 0x96; u8 0x99; u8 0xe2;
      u8 0xf9; u8 0x99; u8 0x4f; u8 0x28; u8 0x0b; u8 0x76; u8 0xcb; u8 0x32; u8 0xb8; u8 0xea;
      u8 0x77; u8 0xad; u8 0xa3; u8 0xe9; u8 0xad; u8 0x82; u8 0x76; u8 0xe3; u8 0x8c; u8 0x4f;
      u8 0x71; u8 0x8f; u8 0xd8; u8 0xd4; u8 0xad; u8 0xb4; u8 0x5b; u8 0x3f; u8 0x84; u8 0xb3;
      u8 0xef; u8 0x91; u8 0x01; u8 0xb4; u8 0xaa; u8 0xfe; u8 0x7b; u8 0xda; u8 0xe3; u8 0x6b;
      u8 0x9e; u8 0x02; u8 0xc2; u8 0xb7; u8 0x35; u8 0xec; u8 0x77; u8 0x15; u8 0xe1; u8 0x13;
      u8 0x95; u8 0x68; u8 0xd4; u8 0x18; u8 0x44; u8 0x29; u8 0x78; u8 0x55; u8 0x47; u8 0xf5;
      u8 0x50; u8 0x98; u8 0x8e; u8 0xf3; u8 0x01; u8 0xa1; u8 0x71; u8 0xf5; u8 0x18; u8 0xa6;
      u8 0xd1; u8 0xfa; u8 0xac; u8 0x90; u8 0xe1; u8 0xa8; u8 0x4d; u8 0x83; u8 0xd7; u8 0xcd;
      u8 0xc5; u8 0x14; u8 0x1d; u8 0xce; u8 0x24; u8 0x9e; u8 0xc4; u8 0x7b; u8 0x15; u8 0x9f;
      u8 0x07; u8 0x3d; u8 0x85; u8 0xf6; u8 0x1b; u8 0x0d; u8 0xe6; u8 0xc1; u8 0x3f; u8 0x1e;
      u8 0x3f; u8 0x6c; u8 0x0a; u8 0xc7; u8 0x2d; u8 0xa4; u8 0x9d; u8 0xb2; u8 0x6e; u8 0x2c;
      u8 0xba; u8 0xb8; u8 0x6f; u8 0xab; u8 0x34; u8 0x3a; u8 0x48; u8 0xab; u8 0x2f; u8 0x75;
      u8 0xab; u8 0x48; u8 0x21; u8 0x8e; u8 0x59; u8 0x9d; u8 0xd0; u8 0xf7; u8 0xcd; u8 0x2d;
      u8 0xed; u8 0xc4; u8 0xb9; u8 0xae; u8 0x1b; u8 0x30; u8 0xf1; u8 0xc6; u8 0x94; u8 0x21;
      u8 0xa7; u8 0x81; u8 0x58; u8 0xcf; u8 0x0e; u8 0x7a; u8 0xf0; u8 0xb5; u8 0x44; u8 0x42;
      u8 0x1a; u8 0xd4; u8 0x22; u8 0xfa; u8 0x18; u8 0x0d; u8 0x2c; u8 0x05; u8 0xd3; u8 0x74;
      u8 0xeb; u8 0x90; u8 0x11; u8 0x25; u8 0xaf; u8 0x00; u8 0x3e; u8 0xe7; u8 0xbe; u8 0xf1;
      u8 0x1e; u8 0xaf; u8 0x6d; u8 0xd0; u8 0x7f; u8 0xa4; u8 0x12; u8 0xcf; u8 0x4f; u8 0xc4;
      u8 0x65; u8 0xaa; u8 0x07; u8 0x73; u8 0x5f; u8 0x22; u8 0xa0; u8 0x32; u8 0xd4; u8 0xd5;
      u8 0xe5; u8 0x28; u8 0x47; u8 0x2e; u8 0xb5; u8 0xc1; u8 0x2d; u8 0x58; u8 0xc2; u8 0xe9;
      u8 0x83; u8 0xcd; u8 0x41; u8 0xa0; u8 0x82; u8 0x63; u8 0x92; u8 0x76; u8 0xc3; u8 0x51;
      u8 0x05; u8 0xf0; u8 0x6f; u8 0x18; u8 0xed; u8 0xb7; u8 0x7b; u8 0x87; u8 0xcb; u8 0x90;
      u8 0x16; u8 0x63; u8 0x3b; u8 0x67; u8 0xc1; u8 0x3a; u8 0xbb; u8 0x66; u8 0x0b; u8 0xcd;
      u8 0x9d; u8 0x9b; u8 0x38; u8 0x7f; u8 0xa1; u8 0x91; u8 0x14; u8 0x07; u8 0x7f; u8 0xcf;
      u8 0x1f; u8 0x11; u8 0x31; u8 0xf7; u8 0x95; u8 0x89; u8 0xf7; u8 0x35; u8 0x34; u8 0x11;
      u8 0xa5; u8 0x5c; u8 0xab; u8 0x70; u8 0x05; u8 0xdd; u8 0x38; u8 0xc1; u8 0x7a; u8 0x42;
      u8 0x89; u8 0x6d; u8 0x13; u8 0xdc; u8 0x16; u8 0xaa; u8 0xbc; u8 0x43; u8 0xc2; u8 0x20;
      u8 0x0f; u8 0xd2; u8 0x21; u8 0x3e; u8 0x15; u8 0x76; u8 0x6f; u8 0x82; u8 0xef; u8 0x29;
      u8 0x96; u8 0x4c; u8 0xd5; u8 0xf4; u8 0x79; u8 0x3a; u8 0x29; u8 0x54; u8 0xab; u8 0xc3;
      u8 0x37; u8 0xbb; u8 0x8c; u8 0x2a; u8 0x86; u8 0x5d; u8 0x76; u8 0x31; u8 0xc8; u8 0xc1;
      u8 0x30; u8 0x47; u8 0x7a; u8 0xce; u8 0x37; u8 0xf0; u8 0xe0; u8 0xe3; u8 0x64; u8 0x6a;
      u8 0xdd; u8 0xb1; u8 0x7d; u8 0x59; u8 0x17; u8 0xee; u8 0xd5; u8 0xfb; u8 0xa9; u8 0x1b;
      u8 0xd6; u8 0x1f; u8 0x70; u8 0x21; u8 0xa7; u8 0xdc; u8 0x55; u8 0x63; u8 0xff; u8 0xdd;
      u8 0xe5; u8 0xb5; u8 0x52; u8 0xc5; u8 0x7d; u8 0x41; u8 0x7e; u8 0x8a; u8 0xdf; u8 0xc1;
      u8 0xf6; u8 0x03; u8 0x8f; u8 0xc7; u8 0x52; u8 0xa3; u8 0xc7; u8 0x66; u8 0x79; u8 0x55;
      u8 0xed; u8 0x0e; u8 0x40; u8 0x59; u8 0xbc; u8 0x60; u8 0x13; u8 0x86; u8 0xb4; u8 0x88;
      u8 0x8c; u8 0xba; u8 0x9b; u8 0x80; u8 0x8a; u8 0x2b; u8 0x4e; u8 0x80; u8 0x92; u8 0xe1;
      u8 0xd2; u8 0x84; u8 0x93; u8 0xb6; u8 0xc8; u8 0xb3; u8 0x23; u8 0x1d; u8 0xd3; u8 0xf7;
      u8 0xdd; u8 0xa6; u8 0x39; u8 0x1a; u8 0x65; u8 0x08; u8 0x0f; u8 0x95; u8 0x78; u8 0x89;
      u8 0xaf; u8 0xab; u8 0xb9; u8 0x9d; u8 0x32; u8 0x89; u8 0x82; u8 0x07; u8 0xf2; u8 0x1d;
      u8 0xc0; u8 0xba; u8 0x30; u8 0x01; u8 0x42; u8 0x9a; u8 0xcc; u8 0x8e; u8 0x16; u8 0x7a;
      u8 0xc0; u8 0xd7; u8 0x4a; u8 0x91; u8 0xe0; u8 0x46; u8 0xf5; u8 0xae; u8 0xe0; u8 0xed;
      u8 0x0a; u8 0x2c; u8 0xe1; u8 0xaf; u8 0x40; u8 0xf1; u8 0x4d; u8 0x18; u8 0x71; u8 0x5e;
      u8 0xd3; u8 0x6c; u8 0x9c; u8 0x52; u8 0x70; u8 0xfd; u8 0xd2; u8 0xac; u8 0x05; u8 0xf6;
      u8 0xcb; u8 0x22; u8 0x9f; u8 0x04; u8 0x8d; u8 0xd0; u8 0x25; u8 0xe1; u8 0xfb; u8 0xed;
      u8 0x19; u8 0x7e; u8 0x65; u8 0x51; u8 0x60; u8 0xcc; u8 0x88; u8 0xce; u8 0xda; u8 0xf5;
      u8 0xad; u8 0xfd; u8 0x63; u8 0xd2; u8 0x62; u8 0x3f; u8 0x98; u8 0x05; u8 0xbf; u8 0xd9;
      u8 0xae; u8 0x16; u8 0x90; u8 0xdb; u8 0x1e; u8 0x15; u8 0x2e; u8 0xb0; u8 0xcd; u8 0x95;
      u8 0x8c; u8 0x27; u8 0x6a; u8 0xd9; u8 0x1b; u8 0xc1; u8 0xdd; u8 0x02; u8 0xa9; u8 0x92;
      u8 0x9a; u8 0x9e; u8 0x2b; u8 0x25; u8 0xeb; u8 0x82; u8 0x65; u8 0xcf; u8 0x5e; u8 0x25;
      u8 0x8c; u8 0x5e; u8 0xc3; u8 0x2a; u8 0x85; u8 0x50; u8 0x67; u8 0x78; u8 0x6c; u8 0xe5;
      u8 0x8f; u8 0xdb; u8 0x56; u8 0xd3; u8 0x73; u8 0x64; u8 0x83; u8 0xaa; u8 0xe6; u8 0x97;
      u8 0x2d; u8 0x90; u8 0x9c; u8 0xb3; u8 0x59; u8 0xf5; u8 0xee; u8 0x59; u8 0xe3; u8 0x05;
      u8 0xb1; u8 0xa1; u8 0x45; u8 0x4c; u8 0xcf; u8 0x94; u8 0x3e; u8 0x5c; u8 0x15; u8 0x06;
      u8 0xf9; u8 0x5c; u8 0xc3; u8 0x82; u8 0x22; u8 0x71; u8 0x2b; u8 0x42; u8 0xb5; u8 0xd5;
      u8 0x44; u8 0x8f; u8 0xf8; u8 0x64; u8 0x54; u8 0x75; u8 0x03; u8 0xcf; u8 0xdd; u8 0x91;
      u8 0x6b; u8 0x05; u8 0x09; u8 0x24; u8 0x7f; u8 0xd5; u8 0x97; u8 0x3e; u8 0xa4; u8 0x7c;
      u8 0x65; u8 0x0a; u8 0x42; u8 0x6b; u8 0x64; u8 0xa2; u8 0xd8; u8 0x81; u8 0x4f; u8 0xc0;
      u8 0xec; u8 0xd8; u8 0x79; u8 0x4c; u8 0xcb; u8 0x9c; u8 0x27; u8 0xbc; u8 0x60; u8 0x6f;
      u8 0xe2; u8 0x49; u8 0x9b; u8 0x44; u8 0x93; u8 0x6d; u8 0xa4; u8 0x74; u8 0x04; u8 0x1c;
      u8 0x81; u8 0xf9; u8 0x01; u8 0x8f; u8 0xd2; u8 0x4d; u8 0xad; u8 0x07; u8 0x9a; u8 0xbb;
      u8 0x11; u8 0xc8; u8 0x76; u8 0x64; u8 0x29; u8 0xfe; u8 0xa4; u8 0x1a; u8 0x25; u8 0x05;
      u8 0x4a; u8 0xaf; u8 0x59; u8 0xa9; u8 0x88; u8 0xf7; u8 0x73; u8 0x12; u8 0x60; u8 0xd4;
      u8 0x12; u8 0x01; u8 0x68; u8 0xf5; u8 0xbe; u8 0xc5; u8 0xb2; u8 0x7b; u8 0xdc; u8 0xeb;
      u8 0x96; u8 0xec; u8 0x43; u8 0x5d; u8 0xc2; u8 0x07; u8 0xb4; u8 0x1d; u8 0xf7; u8 0x78;
      u8 0xa7; u8 0x82; u8 0x8d; u8 0x10; u8 0x0b; u8 0x90; u8 0xeb; u8 0x5c; u8 0x1e; u8 0x49;
      u8 0x7b; u8 0xdd; u8 0x56; u8 0xc7; u8 0x5f; u8 0x0f; u8 0x8f; u8 0x9a; u8 0x21; u8 0xcf;
      u8 0xa4; u8 0x63; u8 0x20; u8 0x0c; u8 0xe5; u8 0xf7; u8 0xc2; u8 0xdf; u8 0xf1; u8 0xec;
      u8 0xf3; u8 0x94; u8 0x5b; u8 0xad; u8 0x29; u8 0xdd; u8 0x0b; u8 0x43; u8 0x19; u8 0xab;
      u8 0x93; u8 0xec; u8 0x7d; u8 0x50; u8 0x6b; u8 0x67; u8 0xf5; u8 0x2f; u8 0xf1; u8 0xe7;
      u8 0x4b; u8 0xe2; u8 0x35; u8 0x41; u8 0x47; u8 0xd8; u8 0xcf; u8 0x9a; u8 0xbb; u8 0x38;
      u8 0x3a; u8 0x37; u8 0xc3; u8 0x61; u8 0x43; u8 0xa4; u8 0x41; u8 0xab; u8 0x4d; u8 0x9b;
      u8 0xd9; u8 0xbf; u8 0x19; u8 0x6e; u8 0x66; u8 0xa1; u8 0xfd; u8 0xef; u8 0x54; u8 0x6f;
      u8 0xef; u8 0x1e; u8 0xe0; u8 0x26; u8 0xab; u8 0xe3; u8 0xf5; u8 0xe7; u8 0x22; u8 0xd0;
      u8 0x84; u8 0x6e; u8 0x78; u8 0x90; u8 0x70; u8 0xc3; u8 0x87; u8 0x6a; u8 0x68; u8 0xb8;
      u8 0x5f; u8 0x80; u8 0x10; u8 0xb3; u8 0x8f; u8 0x56; u8 0xff; u8 0x16; u8 0xf9; u8 0x88;
      u8 0x67; u8 0x1a; u8 0x51; u8 0x3c; u8 0xf8; u8 0x27; u8 0x40; u8 0xbb; u8 0x69; u8 0x6e;
      u8 0xcb; u8 0x80; u8 0xa4; u8 0x0d; u8 0xb6; u8 0xb2; u8 0x66; u8 0xbd; u8 0xa2; u8 0xcb;
      u8 0xfe; u8 0xd7; u8 0x67; u8 0x5f; u8 0xfa; u8 0x85; u8 0xd0; u8 0x98; u8 0x1e; u8 0x5d;
      u8 0x35; u8 0x01; u8 0x91; u8 0x3f; u8 0x91; u8 0x46; u8 0xac; u8 0xcd; u8 0x82; u8 0xd3;
      u8 0xe1; u8 0x5c; u8 0x53; u8 0x66; u8 0xa7; u8 0xa1; u8 0x00; u8 0xd5; u8 0x34; u8 0x3f;
      u8 0x1e; u8 0x1e; u8 0x0f; u8 0x1c; u8 0xef; u8 0x5d; u8 0x2e; u8 0x79; u8 0x28; u8 0x02;
      u8 0xbe; u8 0x9b; u8 0x8b; u8 0xfa; u8 0x5a; u8 0x0a; u8 0xf3; u8 0xfc; u8 0x8c; u8 0xdc;
      u8 0xbd; u8 0xa3; u8 0xb6; u8 0xd3; u8 0x5b; u8 0xe0; u8 0xfb; u8 0xee; u8 0x63; u8 0xd3;
      u8 0x72; u8 0x5a; u8 0xfb; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0x03; u8 0x00;
      u8 0xfe; u8 0xff; u8 0xfd; u8 0xff; u8 0x01; u8 0x00; u8 0xff; u8 0xff; u8 0x02; u8 0x00;
      u8 0x02; u8 0x00; u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0x03; u8 0x00; u8 0xff; u8 0xff;
      u8 0xfb; u8 0xff; u8 0xfe; u8 0xff; u8 0x06; u8 0x00; u8 0x06; u8 0x00; u8 0x01; u8 0x00;
      u8 0xfc; u8 0xff; u8 0xfd; u8 0xff; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x01; u8 0x00;
      u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0xfc; u8 0xff; u8 0x02; u8 0x00; u8 0x04; u8 0x00;
      u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0x03; u8 0x00;
      u8 0x01; u8 0x00; u8 0xfe; u8 0xff; u8 0x04; u8 0x00; u8 0xfe; u8 0xff; u8 0x06; u8 0x00;
      u8 0xff; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff; u8 0x00; u8 0x00;
      u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfe; u8 0xff; u8 0x00; u8 0x00; u8 0xfe; u8 0xff; u8 0x04; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfd; u8 0xff; u8 0x00; u8 0x00; u8 0xff; u8 0xff; u8 0xfb; u8 0xff; u8 0x00; u8 0x00;
      u8 0x01; u8 0x00; u8 0xfe; u8 0xff; u8 0xfb; u8 0xff; u8 0x02; u8 0x00; u8 0x00; u8 0x00;
      u8 0x00; u8 0x00; u8 0xfe; u8 0xff; u8 0xfe; u8 0xff; u8 0xff; u8 0xff; u8 0x06; u8 0x00;
      u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0x02; u8 0x00;
      u8 0x01; u8 0x00; u8 0x01; u8 0x00; u8 0x01; u8 0x00; u8 0xff; u8 0xff; u8 0xff; u8 0xff;
      u8 0x01; u8 0x00; u8 0xfb; u8 0xff; u8 0x05; u8 0x00; u8 0x02; u8 0x00; u8 0xfd; u8 0xff;
      u8 0x02; u8 0x00; u8 0x05; u8 0x00; u8 0xfd; u8 0xff; u8 0x04; u8 0x00; u8 0x02; u8 0x00;
      u8 0x04; u8 0x00; u8 0xfb; u8 0xff; u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0x02; u8 0x00;
      u8 0xfc; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0x02; u8 0x00;
      u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xfc; u8 0xff; u8 0x01; u8 0x00;
      u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0xfd; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00;
      u8 0x04; u8 0x00; u8 0xff; u8 0xff; u8 0xfc; u8 0xff; u8 0x01; u8 0x00; u8 0x03; u8 0x00;
      u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0xff; u8 0xff; u8 0x03; u8 0x00; u8 0xff; u8 0xff;
      u8 0xff; u8 0xff; u8 0xfe; u8 0xff; u8 0xfd; u8 0xff; u8 0x01; u8 0x00; u8 0xfe; u8 0xff;
      u8 0x03; u8 0x00; u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0xfe; u8 0xff;
      u8 0x00; u8 0x00; u8 0xff; u8 0xff; u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0x01; u8 0x00;
      u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0xfe; u8 0xff; u8 0x00; u8 0x00;
      u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0xfa; u8 0xff; u8 0x02; u8 0x00; u8 0x04; u8 0x00;
      u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0x03; u8 0x00; u8 0x08; u8 0x00;
      u8 0xfb; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff; u8 0x08; u8 0x00;
      u8 0x04; u8 0x00; u8 0xfd; u8 0xff; u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0x01; u8 0x00;
      u8 0x04; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xff;
      u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x00;
      u8 0x00; u8 0x00; u8 0x04; u8 0x00; u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0xff; u8 0xff;
      u8 0x01; u8 0x00; u8 0xfd; u8 0xff; u8 0x01; u8 0x00; u8 0xff; u8 0xff; u8 0x01; u8 0x00;
      u8 0x01; u8 0x00; u8 0x06; u8 0x00; u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfe; u8 0xff; u8 0x00; u8 0x00; u8 0x02; u8 0x00; u8 0xfc; u8 0xff; u8 0xff; u8 0xff;
      u8 0x00; u8 0x00; u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfe; u8 0xff; u8 0x05; u8 0x00; u8 0x05; u8 0x00; u8 0xfe; u8 0xff; u8 0x03; u8 0x00;
      u8 0x02; u8 0x00; u8 0x04; u8 0x00; u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0x05; u8 0x00;
      u8 0x02; u8 0x00; u8 0xfc; u8 0xff; u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0xff; u8 0xff;
      u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0xfc; u8 0xff; u8 0xfe; u8 0xff;
      u8 0x02; u8 0x00; u8 0xfc; u8 0xff; u8 0xfe; u8 0xff; u8 0xfd; u8 0xff; u8 0xfc; u8 0xff;
      u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0xfc; u8 0xff;
      u8 0x04; u8 0x00; u8 0x01; u8 0x00; u8 0x04; u8 0x00; u8 0xfd; u8 0xff; u8 0xff; u8 0xff;
      u8 0xfb; u8 0xff; u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0x04; u8 0x00; u8 0x03; u8 0x00;
      u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0xfc; u8 0xff; u8 0x01; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xff; u8 0xff; u8 0xfd; u8 0xff; u8 0x03; u8 0x00; u8 0xff; u8 0xff; u8 0xfe; u8 0xff;
      u8 0x05; u8 0x00; u8 0x01; u8 0x00; u8 0x03; u8 0x00; u8 0xfa; u8 0xff; u8 0x02; u8 0x00;
      u8 0x00; u8 0x00; u8 0xfe; u8 0xff; u8 0xfe; u8 0xff; u8 0x02; u8 0x00; u8 0xfe; u8 0xff;
      u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0x04; u8 0x00; u8 0x01; u8 0x00;
      u8 0x01; u8 0x00; u8 0x06; u8 0x00; u8 0x04; u8 0x00; u8 0xff; u8 0xff; u8 0x02; u8 0x00;
      u8 0xfc; u8 0xff; u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0x00; u8 0x00;
      u8 0x01; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0xfe; u8 0xff; u8 0xfe; u8 0xff;
      u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0x05; u8 0x00; u8 0x01; u8 0x00;
      u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0x01; u8 0x00; u8 0xfe; u8 0xff;
      u8 0xfd; u8 0xff; u8 0x01; u8 0x00; u8 0xfe; u8 0xff; u8 0x03; u8 0x00; u8 0x03; u8 0x00;
      u8 0x02; u8 0x00; u8 0x04; u8 0x00; u8 0x06; u8 0x00; u8 0x01; u8 0x00; u8 0x00; u8 0x00;
      u8 0xfe; u8 0xff; u8 0xfe; u8 0xff; u8 0x02; u8 0x00; u8 0xfe; u8 0xff; u8 0x02; u8 0x00;
      u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0x01; u8 0x00; u8 0x00; u8 0x00;
      u8 0x03; u8 0x00; u8 0xfc; u8 0xff; u8 0xfe; u8 0xff; u8 0xff; u8 0xff; u8 0xfb; u8 0xff;
      u8 0xfd; u8 0xff; u8 0x04; u8 0x00; u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0x01; u8 0x00;
      u8 0xff; u8 0xff; u8 0xfe; u8 0xff; u8 0xff; u8 0xff; u8 0xfc; u8 0xff; u8 0xfc; u8 0xff;
      u8 0x06; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff; u8 0xfd; u8 0xff; u8 0xff; u8 0xff;
      u8 0xfe; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0x03; u8 0x00; u8 0xfb; u8 0xff;
      u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0xfd; u8 0xff; u8 0xfd; u8 0xff; u8 0x02; u8 0x00;
      u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0x03; u8 0x00; u8 0xfc; u8 0xff; u8 0xfb; u8 0xff;
      u8 0x01; u8 0x00; u8 0x04; u8 0x00; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfd; u8 0xff; u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0x01; u8 0x00;
      u8 0xf8; u8 0xff; u8 0x01; u8 0x00; u8 0x00; u8 0x00; u8 0xfe; u8 0xff; u8 0xfc; u8 0xff;
      u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0xfe; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xff;
      u8 0x04; u8 0x00; u8 0x02; u8 0x00; u8 0xfd; u8 0xff; u8 0x01; u8 0x00; u8 0xfd; u8 0xff;
      u8 0x04; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x01; u8 0x00; u8 0x00; u8 0x00;
      u8 0x00; u8 0x00; u8 0x02; u8 0x00; u8 0x01; u8 0x00; u8 0x03; u8 0x00; u8 0x03; u8 0x00;
      u8 0xfa; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0x02; u8 0x00; u8 0xff; u8 0xff;
      u8 0x01; u8 0x00; u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0x04; u8 0x00; u8 0x03; u8 0x00;
      u8 0x01; u8 0x00; u8 0xfe; u8 0xff; u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0xff; u8 0xff;
      u8 0x01; u8 0x00; u8 0x05; u8 0x00; u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0xfd; u8 0xff;
      u8 0x02; u8 0x00; u8 0xfe; u8 0xff; u8 0x03; u8 0x00; u8 0x01; u8 0x00; u8 0x01; u8 0x00;
      u8 0x00; u8 0x00; u8 0x03; u8 0x00; u8 0x03; u8 0x00; u8 0xfe; u8 0xff; u8 0x00; u8 0x00;
      u8 0x02; u8 0x00; u8 0xfc; u8 0xff; u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0xfe; u8 0xff;
      u8 0x04; u8 0x00; u8 0x01; u8 0x00; u8 0x06; u8 0x00; u8 0xfd; u8 0xff; u8 0xfd; u8 0xff;
      u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0xfd; u8 0xff; u8 0xfe; u8 0xff; u8 0xff; u8 0xff;
      u8 0xff; u8 0xff; u8 0xfe; u8 0xff; u8 0x07; u8 0x00; u8 0x01; u8 0x00; u8 0xff; u8 0xff;
      u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0xfc; u8 0xff; u8 0xfd; u8 0xff; u8 0x01; u8 0x00;
      u8 0xff; u8 0xff; u8 0x03; u8 0x00; u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0x03; u8 0x00;
      u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0x00; u8 0x00; u8 0xfe; u8 0xff;
      u8 0xff; u8 0xff; u8 0xfe; u8 0xff; u8 0x02; u8 0x00; u8 0xfb; u8 0xff; u8 0xfc; u8 0xff;
      u8 0x01; u8 0x00; u8 0xff; u8 0xff; u8 0x01; u8 0x00; u8 0x02; u8 0x00; u8 0xfd; u8 0xff;
      u8 0xfe; u8 0xff; u8 0xfb; u8 0xff; u8 0x00; u8 0x00; u8 0xff; u8 0xff; u8 0x03; u8 0x00;
      u8 0x01; u8 0x00; u8 0x03; u8 0x00; u8 0x01; u8 0x00; u8 0x01; u8 0x00; u8 0x01; u8 0x00;
      u8 0xff; u8 0xff; u8 0xfa; u8 0xff; u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0x00; u8 0x00;
      u8 0xfb; u8 0xff; u8 0xff; u8 0xff; u8 0x02; u8 0x00; u8 0xff; u8 0xff; u8 0x00; u8 0x00;
      u8 0xfe; u8 0xff; u8 0x05; u8 0x00; u8 0x05; u8 0x00; u8 0x01; u8 0x00; u8 0xfe; u8 0xff;
      u8 0x01; u8 0x00; u8 0x01; u8 0x00; u8 0x03; u8 0x00; u8 0xfe; u8 0xff; u8 0xff; u8 0xff;
      u8 0xfe; u8 0xff; u8 0x05; u8 0x00; u8 0x02; u8 0x00; u8 0xfc; u8 0xff; u8 0xfe; u8 0xff;
      u8 0x05; u8 0x00; u8 0x01; u8 0x00; u8 0x00; u8 0x00; u8 0xfc; u8 0xff; u8 0x02; u8 0x00;
      u8 0xfe; u8 0xff; u8 0x01; u8 0x00; u8 0xfc; u8 0xff; u8 0x02; u8 0x00; u8 0x01; u8 0x00;
      u8 0x03; u8 0x00; u8 0x00; u8 0x00; u8 0xff; u8 0xff; u8 0xfb; u8 0xff; u8 0xfd; u8 0xff;
      u8 0x00; u8 0x00; u8 0x02; u8 0x00; u8 0x02; u8 0x00; u8 0xfb; u8 0xff; u8 0xfd; u8 0xff;
      u8 0xfd; u8 0xff; u8 0xff; u8 0xff; u8 0x01; u8 0x00
    ]
  in
  createL_global l

let seed: b: ilbuffer uint8 48ul {recallable b} =
  [@ inline_let ]let l =
    [
      u8 0x64; u8 0x33; u8 0x5b; u8 0xf2; u8 0x9e; u8 0x5d; u8 0xe6; u8 0x28; u8 0x42; u8 0xc9;
      u8 0x41; u8 0x76; u8 0x6b; u8 0xa1; u8 0x29; u8 0xb0; u8 0x64; u8 0x3b; u8 0x5e; u8 0x71;
      u8 0x21; u8 0xca; u8 0x26; u8 0xcf; u8 0xc1; u8 0x90; u8 0xec; u8 0x7d; u8 0xc3; u8 0x54;
      u8 0x38; u8 0x30; u8 0x55; u8 0x7f; u8 0xdd; u8 0x5c; u8 0x03; u8 0xcf; u8 0x12; u8 0x3a;
      u8 0x45; u8 0x6d; u8 0x48; u8 0xef; u8 0xea; u8 0x43; u8 0xc8; u8 0x68
    ]
  in
  createL_global l

val main: unit -> St C.exit_code
let main () =
  recall seed;
  recall test1_ss_expected;
  recall test1_pk_expected;
  recall test1_ct_expected;
  recall test1_sk_expected;
  push_frame();
  let seed' = create 48ul (u8 0) in
  copy seed' seed;
  test_frodo seed' test1_ss_expected test1_pk_expected test1_ct_expected test1_sk_expected;
  pop_frame();
  C.EXIT_SUCCESS
